Nuprl Lemma : es-interval_wf2
0,22
postcript
pdf
es
:ES,
e
,
e'
:E. [
e
,
e'
]
{
ev
:E| loc(
ev
) = loc(
e'
)
Id } List
latex
Definitions
x
L
.
P
(
x
)
,
x
:
A
.
B
(
x
)
,
loc(
e
)
,
t
T
,
Id
,
Prop
,
E
,
[
e
,
e'
]
,
P
Q
,
x
.
t
(
x
)
,
ES
,
(
e
<loc
e'
)
,
e
e'
,
P
&
Q
,
P
Q
,
(
x
l
)
,
P
Q
Lemmas
l
member
wf
,
member-es-interval
,
es-E
wf
,
event
system
wf
,
list-set-type2
,
es-interval
wf
,
Id
wf
,
es-loc
wf
origin
es:ES, e, e':E. [e, e'] 
{ev:E| loc(ev) = loc(e') Id } List es:ES, e, e':E. [e, e'] {ev:E| loc(ev) = loc(e') Id } List xL. P(x)x:A. B(x) T
Q
x. t(x)
e' 
Q l)
Q